\documentclass[11pt]{report}

%IMPORTANTE comando \hyphenation{ma-cro-istru-zio-ne nitro-idrossil-amminico} definisce all'algoritmo di latex come spezzare una parola non presente nel suo vocabolario!!

%INCLUSIONE DI PACCHETTI
\usepackage{graphicx}
\usepackage{rotating}
\usepackage{array}
\usepackage{longtable}
\usepackage{multirow}
\usepackage{wrapfig} 
\usepackage{lastpage}
\usepackage{fancyhdr}
\usepackage[english]{babel}
\usepackage{amssymb}
%\usepackage[T1]{fontenc}
%\usepackage[latin9]{inputenc}
\usepackage[colorlinks=true]{hyperref} %per indice con link alle pagine
\usepackage[a4paper,portrait,left=2.5cm,right=2.5cm,bindingoffset=5mm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{color}
%\usepackage{xstring}
\hypersetup{colorlinks,citecolor=black,filecolor=black,linkcolor=red,urlcolor=blue}
\setcounter{secnumdepth}{2} % per numerare anche \subsubsection
\setcounter{tocdepth}{2}% per farlo apparire nell'indice
\frenchspacing
\definecolor{LightMagenta}{cmyk}{0.1,0.8,0,0.1}


%HEADER e FOOTER di tutte le pagine tranne quella in cui compare il titolo del capitolo
\pagestyle{fancy}
\fancyhead{}
\headheight = 54pt
\lhead{Computer Science Theory II}
\lfoot{}
\cfoot{}
\rfoot{Page \thepage{ of} \pageref{LastPage}}
\renewcommand{\headrulewidth}{1pt}
\renewcommand{\footrulewidth}{1pt}
\rhead{\nouppercase{\leftmark}}
\renewcommand{\chaptermark}[1]{\markboth{\thechapter.\ #1}{}}

%HEADER e FOOTER della pagina dove compare il titolo del capitolo
\fancypagestyle{plain}{
%\lhead{\includegraphics[height=50pt]{images/logoUniPd.png}} %IN ALTO A SINISTRA (POTREBBE ANDARE BENE IL LOGO)
\chead{}
\rhead{\bfseries WS2011/12}%\manualeUtenteVer} %IN ALTO A DESTRA
\lfoot{
\begin{tabular}{lc}
Victor A. Arrascue Ayala & Mtr. 3209050\\
Tobias Domhan  & Mtr.  3202957 \\
\end{tabular}
}
\cfoot{}
\rfoot{Page \thepage{ of} \pageref{LastPage}}
\renewcommand{\headrulewidth}{1pt}
\renewcommand{\footrulewidth}{1pt}
}

\fancypagestyle{romano}{
\lhead{}
\chead{}
\rhead{}
\lfoot{}
\cfoot{\thepage}
\rfoot{}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
}

\fancypagestyle{empty}{
\lhead{}
\chead{}
\rhead{}
\lfoot{}
\cfoot{}
\rfoot{}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
}

%PAGINA DI PRESETAZIONE DEL DOCUMENTO
\hyphenation{}
\begin{document}


%\begin{center}
%\thispagestyle{empty}
%\huge\textbf{UNIVERSIT\`A degli Studi di PADOVA}\\[2 cm] %GRUPPO DI APPARTENENZA
%\vspace*{0.5in}
%\LARGE\textbf{Titolo del documento}\\[1.0 cm] %TITOLO DEL DOCUMENTO
%\par\rule{10cm}{.5pt} \par
%{\large 12 Ottobre 2009}   %DATA DI CREAZIONE
%\par\rule{10cm}{.10pt} \par
%\vspace*{1.0in}
%\includegraphics[scale=0.30]{images/logoUniPd.png} \\[2cm] %LOGO GRUPPO
%\Large\textbf{Michele Tonon} %AUTORE
%\par\rule{6cm}{.5pt} \par
%\end{center}



% INDEX
%\newpage
%\thispagestyle{romano}
%\pagenumbering{arabic}
%\tableofcontents


%--------------------------------------------- 


%CONTENT


\newpage
\thispagestyle{plain}

\begin{center}
{\Large \textbf{Exercise Sheet 3}}
\end{center}

\noindent{\textbf{Exercise 3.1}}\\\\
Proof:\\
``$_{\Rightarrow}$": The premise is that KB $\cup$ \{$\varphi$\} is unsatisfiable. We must show that KB $\vDash$ $\neg$$\varphi$. Consider any such model I of KB.\\
I cannot be a model of KB $\cup$ \{$\varphi$\}, because by the premise it is unsatisfiable. That means that I $\nvDash$$\varphi$, which is equivalent to I  $\vDash$ $\neg$$\varphi$. Since this property holds for every I model of KB, then KB $\vDash$ $\neg$$\varphi$.\\\\
``$_{\Leftarrow}$": The premise is that KB $\vDash$ $\neg$$\varphi$. We must show that KB $\cup$ \{$\varphi$\} is unsatisfiable.\\
Since KB $\vDash$ $\neg$$\varphi$, then all models I of KB are models of $\neg$$\varphi$ and we can state that I  $\vDash$ $\neg$$\varphi$. But then I $\nvDash$$\varphi$. Since KB and $\varphi$ have no common models, we can say that KB $\cup$ \{$\varphi$\} is unsatisfiable.\\\\
\noindent{\textbf{Exercise 3.2}}\\\\
The knowledge base looks like this:\\
$ KB = \{A, B, A \vee C, K \wedge E \leftrightarrow A \wedge B, \neg C \rightarrow D, E \vee F \rightarrow \neg D \} $
\\\\
We would like to derive the following:\\
$\phi = B \wedge C$\\
\vspace{0.1cm}

\begin{tabular}{lc}
  and introduction & $\frac{A, B}{A \wedge B}$\\
\\
  modus ponens & $\frac{A \wedge B, A \wedge B \rightarrow K \wedge E}{K \wedge E}$\\
\\
  and elimination & $\frac{K \wedge E}{K, E}$\\
\\
  or introduction & $\frac{E}{E \vee F}$\\
\\
  modus ponens & $\frac{E \vee F, E \vee F \rightarrow \neg D}{\neg D}$\\
\\
  modus tollens & $\frac{\neg D, \neg C \rightarrow D}{C}$\\
\\and introduction & $\frac{C, B}{C \wedge B}$\\
\end{tabular}

\vspace{1cm}
\noindent{\textbf{Exercise 3.3}}\\\\
(a)\\
1. eliminating $\rightarrow$ and $\leftrightarrow$ results in:
\[
\neg(\neg p \wedge \neg r) \wedge (\neg r \vee q) \wedge \neg q \wedge (\neg p \vee t) \wedge \neg s \wedge (\neg t \vee s) 
\]
2. moving all negations inline:
\[
(p \vee r) \wedge (\neg r \vee q) \wedge \neg q \wedge (\neg p \vee t) \wedge \neg s \wedge (\neg t \vee s) 
\]
This already results in CNF. Hence, we will skip step 3.\\\\
(b)\\
We assume that the CNF formula represents our KB. Using the logical notation for sets of clauses:\\
$\triangle$ = \{ \{p, r\}, \{ $\neg$r, q \},  \{$\neg$q\}, \{$\neg$p, t\}, $\{\neg$s\}, \{$\neg$t, s\} \}\\
where C1 =  \{p, r\}, C2 = \{$\neg$r, q \}, ... , C6 = \{$\neg$t, s\} \\
C7 = \{r, t\} from C1 and C4\\
C8 = \{r, s\} from C6 and C7\\
C9 = \{s, q\} from C2 and C8\\
C10 =\{ q \} from C5 and C9\\
C11 = $\square$ from C3 and C10\\\\
Since we can derive the empty clause, the original formula $\triangle$ is unsatisfiable.

\end{document}

